The present application relates generally to an improved data processing apparatus and method and more specifically to mechanisms for efficiently determining Boolean satisfiability with lazy constraints.
Boolean satisfiability (SAT) is the problem of finding an assignment to variables such that a system of logic relationships are all true. SAT is used as a subroutine in many Electronic Design Automation algorithms, including algorithms in logic synthesis and verification.
Constraints are logical conditions that are assumed to always hold. Constraints are used for applications in logic synthesis and verification. Constraints may represent user assumptions either on the operation of a design or on a design environment. Constraints may also represent assumptions that the algorithms themselves make.
Temporal induction, an algorithm used extensively in both logic synthesis and verification, is an example of an algorithm that utilizes constraints. Let A and B be two nets in a design and suppose a presumption is made that A=B. A check may be made that A=B in all reachable states using temporal induction: the “base case” involves checking that A=B holds in all initial states, and the “inductive step” involves checking that for all state transitions S1→S2, if A=B on S1 then A=B on S2. Often the inductive step is implemented using a constraint that A=B on S1. Temporal induction commonly checks many equivalences simultaneously, leading to a large number of constraints.
Constraints can be applied in SAT by conjoining the constraint with the original problem. Conjoining the constraint with the original problem enlarges the effective SAT problem and forces the solver to satisfy both the original problem and all constraints. When the number of constraints is large, the size of this effective SAT problem may be dominated by the constraints alone. The large effective problem size may also mean that the runtime of SAT is undesirably long.